我们介绍了ERHL,这是一种程序逻辑,用于推理有关对概率计划的关系期望属性的推理。erhl是定量的,即,其前后条件在扩展的非阴性实物中具有值。由于其定量断言,ERHL克服了先前逻辑中的随机性对齐限制,包括PRHL,PRHL是一种流行的关系程序逻辑,用于推理密码构造的安全性,而APRHL是PRHL的prHL变体,用于差异nifential隐私。结果,ERHL是第一个关系概率的程序逻辑,可以得到所有几乎所有肯定终止程序的非平凡的健全性和完整性结果的支持。我们表明,相对于程序等效性,统计距离和差异隐私而言,ERHL是合理且完整的。我们还表明,每个PRHL判断都是有效的。我们展示了ERHL的实际收益,其中包括PRHL和APRHL无法实现的示例。
主要关键词